﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.InternalClass
{
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class InnerClassTest1
    {
        /// <summary>
        /// A scenario where the not-covered branching condition appears from the external
        /// method, but the actual situation is from the inner one. How to deal with this situation?
        /// 
        /// Current Result: As a field of type an internal class is involved, the corresponding
        /// call-back due to un-covered branch is not getting invoked. Pex ISSUE.
        /// </summary>
        /// <param name="os"></param>
        [PexAssertReachEventually]
        [PexMethod]        
        public void InnerClassTestPUT([PexAssumeUnderTest]OuterStack os)
        {
            if (os.Size() > 1)
                PexAssert.ReachEventually();
        }

        [PexAssertReachEventually]
        [PexMethod]
        public void InnerClassVariantPUT([PexAssumeUnderTest]OuterStackVariant isv)
        {
            if (isv.Size() > 1)
                PexAssert.ReachEventually();
        }
    }
}
